Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems. In this paper, the model-checking problem for the modal $\mu$-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal $\mu$-calculus, parity games on hierarchically defined input graphs are investigated. In most cases precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented.
展开▼
机译：分层图定义允许使用模块来重复描述子结构，从而对图进行模块化描述。除了这种模块化之外，层次图定义还允许使用多项式大小描述来指定指数大小的图。在许多情况下，这种简洁性增加了决策问题的计算复杂性。在本文中，研究了分层定义的输入图上模态$ \ mu $-微积分和（单子）最小不动点逻辑的模型检查问题。为了分析模态微积分，研究了分层定义的输入图上的奇偶博弈。在大多数情况下，可以得出精确的上下复杂度界限。提出了对分层图定义的限制，该限制导致使用更有效的模型检查算法。
展开▼
